P:Prop, p:Dec(P). {dec2bool(p)  P} 

latex

Definitions	{T}, Dec(P), dec2bool(d), P  Q, P  Q, P & Q, P  Q, true, false, x:A. B(x), b, True, t  T, A, P  Q, Prop, False
Lemmas	not wf, bfalse wf, btrue wf, assert wf